{-# LANGUAGE TemplateHaskell, TypeFamilies, TypeOperators, GADTs,
  FlexibleInstances, MultiParamTypeClasses, FlexibleContexts, UndecidableInstances,
  TypeSynonymInstances, EmptyDataDecls #-}

{-# OPTIONS_GHC -fcontext-stack=250 #-}

{- |

Module      :  Examples.TermGeneric
Copyright   :  (c) The University of Kansas 2011
License     :  BSD3

Maintainer  :  nicolas.frisby@gmail.com
Stability   :  experimental
Portability :  see LANGUAGE pragmas (... GHC)

The declaration that hook 'Examples.TermBase.Type', 'Examples.TermBase.Term',
and 'Examples.TermBase.Decl' into @yoko@. This will eventually be generated via
Template Haskell.

-}
module Examples.TermGeneric where

import qualified Examples.TermBase as B

import Examples.ReflectAux

data TBool; data TInt; data TArrow
data Lam; data Var; data App; data Let
data Decl

concat `fmap` mapM derive
  [''B.Type, ''TBool, ''TInt, ''TArrow,
   ''B.Term, ''Lam, ''Var, ''App, ''Let,
   ''B.Decl, ''Decl]

type instance Tag TBool = $(return $ encode "TBool")
type instance Range TBool = B.Type
instance DC TBool where
  occName _ = "TBool"
  fr _ = B.TBool
data instance RM m (N TBool) = TBool
type instance Tag TInt = $(return $ encode "TInt")
type instance Range TInt = B.Type
instance DC TInt where
  occName _ = "TInt"
  fr _ = B.TInt
data instance RM m (N TInt) = TInt
type instance Tag TArrow = $(return $ encode "TArrow")
type instance Range TArrow = B.Type
instance DC TArrow where
  occName _ = "TArrow"
  fr ~(TArrow d r) = B.TArrow d r
data instance RM m (N TArrow) = TArrow (Med m B.Type) (Med m B.Type)
data instance DCs B.Type dc where
  TBool_ :: DCs B.Type TBool; TInt_ :: DCs B.Type TInt
  TArrow_ :: DCs B.Type TArrow
type instance DTs B.Type = TypeDTs
instance DT B.Type where
  packageName _ = "datatype-reflect"
  moduleName _ = "TermBase"
  disband B.TBool        = disbanded TBool
  disband B.TInt         = disbanded TInt
  disband (B.TArrow d r) = disbanded $ TArrow d r
type instance Fin (DCs B.Type) = (:=:) TBool :|| (:=:) TInt :|| (:=:) TArrow
instance Finite (DCs B.Type) where
  toFin TBool_ = membership; toFin TInt_ = membership; toFin TArrow_ = membership
  predFin _ _ x = x
instance Etinif (DCs B.Type) where
  frFin x = case x of
    LeftU          Refl -> TBool_
    RightU (LeftU  Refl) -> TInt_
    RightU (RightU Refl) -> TArrow_

data TypeDTs t where Type__ :: TypeDTs B.Type
type instance Fin TypeDTs = (:=:) B.Type
instance Finite TypeDTs where toFin Type__ = membership; predFin _ _ x = x
instance Etinif TypeDTs where frFin Refl = Type__

finite_set [t|TypeDTs|]

type instance Tag Lam = $(return $ encode "Lam")
type instance Range Lam = B.Term
instance DC Lam where
  occName _ = "Lam"
  fr ~(Lam ty tm) = B.Lam ty tm
data instance RM m (N Lam) = Lam B.Type (Med m B.Term)
type instance Tag Var = $(return $ encode "Var")
type instance Range Var = B.Term
instance DC Var where
  occName _ = "Var"
  fr ~(Var i) = B.Var i
data instance RM m (N Var) = Var Int
type instance Tag App = $(return $ encode "App")
type instance Range App = B.Term
instance DC App where
  occName _ = "App"
  fr ~(App tm0 tm1) = B.App tm0 tm1
data instance RM m (N App) = App (Med m B.Term) (Med m B.Term)
type instance Tag Let = $(return $ encode "Let")
type instance Range Let = B.Term
instance DC Let where
  occName _ = "Let"
  fr ~(Let ds tm) = B.Let ds tm
data instance RM m (N Let) = Let [Med m B.Decl] (Med m B.Term)
data instance DCs B.Term dc where
  Lam_ :: DCs B.Term Lam; Var_ :: DCs B.Term Var
  App_ :: DCs B.Term App; Let_ :: DCs B.Term Let
type instance DTs B.Term = ASTU
instance DT B.Term where
  packageName _ = "datatype-reflect"
  moduleName _ = "TermBase"
  disband (B.Lam ty tm)   = disbanded $ Lam ty tm
  disband (B.Var i)       = disbanded $ Var i
  disband (B.App tm0 tm1) = disbanded $ App tm0 tm1
  disband (B.Let ds tm)   = disbanded $ Let ds tm
type instance Fin (DCs B.Term) =
  ((:=:) Lam :|| (:=:) Var) :|| ((:=:) App :|| (:=:) Let)
instance Finite (DCs B.Term) where
  toFin Lam_ = membership; toFin Var_ = membership
  toFin App_ = membership; toFin Let_ = membership
  predFin _ _ x = x
instance Etinif (DCs B.Term) where
  frFin x = case x of
    LeftU  (LeftU Refl) -> Lam_
    LeftU  (RightU Refl) -> Var_
    RightU (LeftU Refl) -> App_
    RightU (RightU Refl) -> Let_

type instance Tag Decl = $(return $ encode "Decl")
type instance Range Decl = B.Decl
instance DC Decl where
  occName _ = "Decl"
  to = Just . uniqueDC; fr ~(Decl ds tm) = B.Decl ds tm
data instance RM m (N Decl) = Decl B.Type (Med m B.Term)
data instance DCs B.Decl dc where Decl_ :: DCs B.Decl Decl
type instance DTs B.Decl = ASTU
instance DT B.Decl where
  packageName _ = "datatype-reflect"
  moduleName _ = "DeclBase"
  disband ~(B.Decl ty tm) = disbanded $ Decl ty tm
type instance Fin (DCs B.Decl) = (:=:) Decl
instance Finite (DCs B.Decl) where toFin Decl_ = membership; predFin _ _ x = x
instance Etinif (DCs B.Decl) where frFin Refl = Decl_

data ASTU t where Term__ :: ASTU B.Term; Decl__ :: ASTU B.Decl
type instance Fin ASTU = (:=:) B.Term :|| (:=:) B.Decl
instance Finite ASTU where
  toFin Term__ = membership; toFin Decl__ = membership
  predFin _ _ x = x
instance Etinif ASTU where
  frFin x = case x of LeftU Refl -> Term__; RightU Refl -> Decl__

finite_set [t|ASTU|]



type instance Rep TBool = U
instance Generic TBool where
  rep _ = U
  obj _ = TBool
type instance Rep TInt = U
instance Generic TInt where
  rep _ = U
  obj _ = TInt
type instance Rep TArrow = R B.Type :* R B.Type :* U
instance Generic TArrow where
  rep ~(TArrow ty0 ty1) = R ty0 :* R ty1 :* U
  obj ~(R ty0 :* R ty1 :* U) = TArrow ty0 ty1

type instance Rep Var = D Int :* U
instance Generic Var where
  rep ~(Var i) = D i :* U
  obj ~(D i :* U) = Var i
type instance Rep Lam = D B.Type :* R B.Term :* U
instance Generic Lam where
  rep ~(Lam ty tm) = D ty :* R tm :* U
  obj ~(D ty :* R tm :* U) = Lam ty tm
type instance Rep App = R B.Term :* R B.Term :* U
instance Generic App where
  rep ~(App tm0 tm1) = R tm0 :* R tm1 :* U
  obj ~(R tm0 :* R tm1 :* U) = App tm0 tm1
type instance Rep Let = F [] (R B.Decl) :* R B.Term :* U
instance Generic Let where
  rep ~(Let ds tm) = F (map R ds) :* R tm :* U
  obj ~(F rds :* R tm :* U) = Let (map unR rds) tm

type instance Rep Decl = D B.Type :* R B.Term :* U
instance Generic Decl where
  rep ~(Decl ty tm) = D ty :* R tm :* U
  obj ~(D ty :* R tm :* U) = Decl ty tm
